report an error when a type annotation is too general #2109
Conversation
Codecov Report
@@ Coverage Diff @@
## main #2109 +/- ##
=======================================
Coverage 76.98% 76.98%
=======================================
Files 425 425
Lines 13769 13778 +9
Branches 1881 1884 +3
=======================================
+ Hits 10600 10607 +7
- Misses 3169 3171 +2
📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala
Outdated
Show resolved
Hide resolved
| // @type: a => b; | ||
| // @type: a => a; | ||
| // let F == lambda x \in Set(a): ((c, c) => c) x d in F(Int) |
There was a problem hiding this comment.
For my own edification: I don't know how to read the body of this lambda. What is ((c, c) => c) x d? It looks like it's applying an implication to two arguments? Or is that only on the type level? But then what's the labmda doing? And how does F end up being typed as the identify function?
There was a problem hiding this comment.
This expression is written in the syntax of EtcExpr, a lambda calculus over types. The body of the lambda is an application of x and d to a type, which in this case is an operator of two arguments of type c and returns type c.
There was a problem hiding this comment.
It is an identity from the types of view.
There was a problem hiding this comment.
Thank you for explaining. It helps a lot. So is the lambda here a type-level lambda? It seems like it's kind of mixing type level syntax with pseudo-TNT syntax, or am I just totally missing the thread here :D?
It is an identity from the types of view.
So, we are maybe getting outside the scope of this PR, but one thing that I think is throwing me off here is that, afaik, it is not possible to write an operator that actually has type a => a and also relies on some constant d that comes from outside the operator.
The only way we can write an operator of type a => a is if we treat the provided argument as fully abstract, because we can't know anything about the value of type a, since we don't know what type it is (or, equivalently, it must work for any type). So afaik, there would be no way of having a d available that could work for any possible type for application to (c, c) => c. afaiu, This is why (in a HM-ish type system) any function with type a => a must be (isomorphic to) the identity function.
The fact that this test is going through makes me think that either our type inference is off, or we're constructing type here that shouldn't actually be possible to assign to any expression (or else I am just quite confused about what is going on here). But in any of these three cases, it seems like we might be looking to either fix the test, fix the type inference, or fix my understanding :)
| // @type: a => a; | ||
| // let F == lambda x \in Set(a): ((c, c) => c) x d |
There was a problem hiding this comment.
Same question here: I may be being dense, but I don't understand how it is that F here turns out to be the identity function. Is (c, c) => c somehow the k combinator?
There was a problem hiding this comment.
It's the same thing again. We have a lambda that applies an operator of type (c, c) => c) to x and d. We are interested not in the structure of this operator, but only in its type.
There was a problem hiding this comment.
That helps a bit, but the annotation here is really quite confusing, imo, as it seems to be mixing up value and type level syntax. Would this comment convey the same thing but within using types to stand in for expressions?
| // @type: a => a; | |
| // let F == lambda x \in Set(a): ((c, c) => c) x d | |
| // @type: (c, c) => c; | |
| // let G(a, b) = a | |
| // @type: a => a; | |
| // let F == lambda x \in Set(a): G x d |
In any case, I can see that this comment is not change by this PR, so it should be outside the scope of the PR. You've cleared up my confusion, thanks.
The part of this that should perhaps be addressed (at least in discussion) is described in #2109 (comment).
tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala
Outdated
Show resolved
Hide resolved
tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <shon@informal.systems>
tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala
Outdated
Show resolved
Hide resolved
…/TestEtcTypeChecker.scala
Closes #2102. This PR adds a small test in
EtcTypeCheckerthat ensures that a polymorphic type annotation is as precise as the inferred principal type.The new version of the type checker has found a bug in the type annotation of
ReduceSetof__rewire_finite_sets_ext_in_apalache.tla. Due to the incorrect order of arguments, the type was more specific. This is actually a bug in the community modules.Also, it found a bug in our type annotation of
FoldLeftinSequencesExt. This is purely a bug in the type annotation, not propagated to the community modules.Tests added for any new code
Ran
make fmt-fix(or had formatting run automatically on all files edited)Documentation added for any new functionality
Entries added to
./unreleased/for any new functionality